$\forall$${\it es}$:ES, $P_{1}$, $P_{2}$, $Q_{1}$, $Q_{2}$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P_{1}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{1}$($e$)\} ).
\\[0ex]($\forall$$e$:E. ($P_{1}$($e$)) $\Leftarrow\!\Rightarrow$ ($P_{2}$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($Q_{1}$($e$)) $\Leftarrow\!\Rightarrow$ ($Q_{2}$($e$)))
\\[0ex]$\Rightarrow$ ($Q_{1}$ $\leftarrow\leftarrow$ $f$$--$ $P_{1}$ $\Leftarrow\!\Rightarrow$ $Q_{2}$ $\leftarrow\leftarrow$ $f$$--$ $P_{2}$)